package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.ClockGuard;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.SimpleClockGuard;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class HOTAS {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("HOTAS");
		 
		 // Clocks and their guards
		 
		 tiosts.addClock("clock0");	
         SimpleClockGuard guard1 = new SimpleClockGuard(1, "clock0", Constants.GUARD_LT, "5000");
 		 ClockGuard clockGuard1 = new ClockGuard();
 		 clockGuard1.addSimpleClockGuard(guard1);
 		 
         SimpleClockGuard guard2 = new SimpleClockGuard(1, "clock0", Constants.GUARD_LEQ, "40000");
 		 ClockGuard clockGuard2 = new ClockGuard();
 		 clockGuard2.addSimpleClockGuard(guard2); 		 
		 
         // Variables
         TypedData targetHOTAS = new TypedData("targetHOTAS", Constants.TYPE_INTEGER);
         tiosts.addVariable(targetHOTAS);
         TypedData azimuthHOTAS = new TypedData("azimuthHOTAS", Constants.TYPE_INTEGER);
         tiosts.addVariable(azimuthHOTAS);
         TypedData elevationHOTAS = new TypedData("elevationHOTAS", Constants.TYPE_INTEGER);
         tiosts.addVariable(elevationHOTAS);         
         
         // Parameters
         TypedData id = new TypedData("id", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(id);
         TypedData a = new TypedData("a", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(a);
         TypedData e = new TypedData("e", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(e);
         
         // Input, output, and internal actions
         Action init = new Action("init1", Constants.ACTION_INTERNAL);
         tiosts.addAction(init);
         Action selectHOTAS = new Action("selectHOTAS", Constants.ACTION_OUTPUT);
         selectHOTAS.addParameter(id.getName());
         tiosts.addAction(selectHOTAS);
         Action pushButton = new Action("pushButton", Constants.ACTION_INPUT);
         tiosts.addAction(pushButton);
         Action releaseButton = new Action("releaseButton", Constants.ACTION_OUTPUT);
         tiosts.addAction(releaseButton);
         Action finishHOTAS = new Action("finishHOTAS", Constants.ACTION_OUTPUT);
         tiosts.addAction(finishHOTAS);
         Action undesignate = new Action("undesignate", Constants.ACTION_INPUT);
         undesignate.addParameter(id.getName());
         tiosts.addAction(undesignate);
         Action designate = new Action("designate", Constants.ACTION_OUTPUT);
         designate.addParameter(id.getName());
         tiosts.addAction(designate);         
         Action read = new Action("read", Constants.ACTION_INPUT);
         read.addParameter(a.getName());
         read.addParameter(e.getName());
         tiosts.addAction(read);
         Action reticlePositionHotas = new Action("reticlePositionHotas", Constants.ACTION_OUTPUT);
         reticlePositionHotas.addParameter(a.getName());
         reticlePositionHotas.addParameter(e.getName());
         tiosts.addAction(reticlePositionHotas); 
                  
         // Locations
         Location start = new Location("Start1");
         tiosts.addLocation(start);
         Location s0 = new Location("S0");
         tiosts.addLocation(s0);
         Location s1 = new Location("S1");
         tiosts.addLocation(s1);     
         Location s2 = new Location("S2");
         tiosts.addLocation(s2);
         Location s3 = new Location("S3");
         tiosts.addLocation(s3); 
         Location s4 = new Location("S4");
         tiosts.addLocation(s4); 
         Location s5 = new Location("S5");
         tiosts.addLocation(s5); 
         
         // Initial Condition
         tiosts.setInitialCondition("v1 > 0");
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("Start1", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S0");
         tiosts.createTransition("S0",  Constants.GUARD_TRUE, Constants.GUARD_TRUE, selectHOTAS, "targetHOTAS := id", null, Constants.DEADLINE_LAZY, "S1");
         tiosts.createTransition("S1",  Constants.GUARD_TRUE, Constants.GUARD_TRUE, pushButton, null, "clock0 := 0", Constants.DEADLINE_LAZY, "S2");
         tiosts.createTransition("S2",  Constants.GUARD_TRUE, clockGuard1, releaseButton, null, null, Constants.DEADLINE_LAZY, "S3");
         tiosts.createTransition("S3",  Constants.GUARD_TRUE, clockGuard1, finishHOTAS, null, "clock0 := 0", Constants.DEADLINE_LAZY, "S0");
         tiosts.createTransition("S1",  "targetHOTAS = id", Constants.GUARD_TRUE, designate, null, null, Constants.DEADLINE_LAZY, "S4");
         tiosts.createTransition("S4",  Constants.GUARD_TRUE, Constants.GUARD_TRUE, read, "azimuthHOTAS := a | elevationHOTAS := e", null, Constants.DEADLINE_LAZY, "S5");
         tiosts.createTransition("S5", "azimuthHOTAS = a AND elevationHOTAS = e", Constants.GUARD_TRUE, reticlePositionHotas, null, null, Constants.DEADLINE_LAZY, "S3");
         tiosts.createTransition("S1",  Constants.GUARD_TRUE, Constants.GUARD_TRUE, undesignate, "targetHOTAS := id", null, Constants.DEADLINE_LAZY, "S3");
         
         return tiosts;
		 
	 }

}
